Nuprl Definition : R-self-interface 0,22

R-self-interface(R)
== case R of 
== Rnone => True
== Rplus(left,right)=>rec1,rec2.rec1 & rec2
== Rinit(loc,T,x,v)=> True
== Rframe(loc,T,x,L)=> True
== Rsframe(lnk,tag,L)=> True
== Reffect(loc,ds,knd,T,x,f)=> True
== Rsends(ds,knd,T,l,dt,g)=> isrcv(knd lnk(knd) = l  dt(tag(knd))?Void  T
== Rpre(loc,ds,a,T,P)=> True
== Raframe(loc,k,L)=> True
== Rbframe(loc,k,L)=> True
== Rrframe(loc,x,L)=> True 
latex



clarification:

R-self-interface(R)
== case R of 
== Rnone => True
== Rplus(left,right)=>rec1,rec2.rec1 & rec2
== Rinit(loc,T,x,v)=> True
== Rframe(loc,T,x,L)=> True
== Rsframe(lnk,tag,L)=> True
== Reffect(loc,ds,knd,T,x,f)=> True
== Rsends(ds,knd,T,l,dt,g)=> isrcv(knd)
== Rsends(ds,knd,T,l,dt,g)=>  lnk(knd) = l  IdLnk
== Rsends(ds,knd,T,l,dt,g)=>  fpf-cap(dt;IdDeq;tag(knd);Void)  T
== Rpre(loc,ds,a,T,P)=> True
== Raframe(loc,k,L)=> True
== Rbframe(loc,k,L)=> True
== Rrframe(loc,x,L)=> True 
latex


Definitionses realizer ind, P & Q, b, isrcv(k), P  Q, s = t, IdLnk, lnk(k), f(x)?z, IdDeq, tag(k), Void, True
FDL editor aliasesR-self-interface

origin